(* $Id$ *)

(** The following will be imported from the standard library in the future. *)

(* [&] decides the boolean conjunction. *)
deferred val & : (bool * bool) -> bool
where (forall (x, y). pre (&) (x, y))
  and (forall (x, y, b). post (&) (x, y) (b) <=> ((b = true) <=> (x = true and y = true)))

(* [+'] computes the addition between two integers. *)
deferred val +? : (int * int) -> int
where (forall (x, y). pre (+?) (x, y))
  and (forall (x, y, z). post (+?) (x, y) (z) <=> z = x + y)

(* [-'] computes the substraction between two integers. *)
deferred val -? : (int * int) -> int
where (forall (x, y). pre (-?) (x, y))
  and (forall (x, y, z). post (-?) (x, y) (z) <=> z = x - y)

(* [max] is the logical function that returns the maximum of two integers. *)
deferred logic max  : (int * int) ~> int
where forall (x, y). (x <= y <=> max (x, y) = y) and (y <= x <=> max (x, y) = x)

lemma max_disj: forall (x, y). max (x, y) = x or max (x, y) = y

(* [max'] is the implementation of the [max] logical function. *)
deferred val max? : (int * int) -> int
where (forall (x, y). pre (max?) (x, y))
  and (forall (x, y, z). post (max?) (x, y) (z) <=> z = max (x, y))

(* The bounded distance between two integers. *)
deferred predicate dist : (int * int * int) ~> prop
where forall (x, y, p). dist (x, y, p) <=> ((x - y >= (0 - p) and (x - y) <= p))

(* Comparison operators over integers. *)
deferred val <=?  : (int * int) -> bool where
    (forall (x, y, b). (post (<=?) (x, y) (b)) <=> (b = true <=> (x <= y)))
and (forall (x, y). pre (<=?) (x, y))

deferred val >=?  : (int * int) -> bool where
    (forall (x, y). (post (>=?) (x, y) (true)  <=> x >= y))
and (forall (x, y). (post (>=?) (x, y) (false) <=> not (x >= y)))
and (forall (x, y). pre (>=?) (x, y))

deferred val >?   : (int * int) -> bool where
    (forall (x, y). (post (>?) (x, y) (true)  <=> x > y))
and (forall (x, y). (post (>?) (x, y) (false) <=> not (x > y)))
and (forall (x, y). pre (>?) (x, y))

deferred val =?   : (int * int) -> bool
where (forall (x, y). pre ( =? ) (x, y))
  and (forall (x, y). post (=?) (x, y) (true) <=> x = y)
  and (forall (x, y). post (=?) (x, y) (false) <=> not (x = y))

(** Elements of the sets. *)

(* The type of the elements. *)
deferred type elt : *

(* Their equality is decidable. *)
deferred val =elt?  : (elt * elt) -> bool
where (forall x. pre (=elt?) (x))
  and (forall (x, y). post (=elt?) (x, y) (true) <=> x = y)
  and (forall (x, y). post (=elt?) (x, y) (false) <=> not (x = y))

(* There exists an order. *)
deferred predicate <elt : (elt * elt) ~> prop
where (forall x. not (x <elt x))
  and (forall (x, y). (not (x <elt y) and not (x = y)) => y <elt x)
  and (forall (x, y, z). (x <elt y and y <elt z) => x <elt z)
  and (forall (x, y). (x <elt y) or (y <elt x) or (x = y))

(* This order is decidable. *)
deferred val <elt? : (elt * elt) -> bool where
    (forall (x, y). (post (<elt?) (x, y) (true)  <=> x <elt y))
and (forall (x, y). (post (<elt?) (x, y) (false) <=> not (x <elt y)))
and (forall (x, y). pre (<elt?) (x, y))

(** The sets. *)

(* The type of an abstract set. *)
deferred type set : *

(* The membership predicate. *)
deferred predicate %in : (elt * set) ~> prop

(* The empty set. *)
deferred val empty : set
where forall x [x]. not (x %in empty)

deferred logic singleton : elt ~> set
where forall (x, y). x %in (singleton (y)) <=> (x = y)

deferred logic @ : (set * set) ~> set
where forall (s1, s2, x). x %in (s1 @ s2) <=> ((x %in s1) or (x %in s2))

deferred logic ^ : (set * set) ~> set
where forall (s1, s2, x). x %in (s1 ^ s2) <=> ((x %in s1) and (x %in s2))

deferred logic \\ : (set * set) ~> set
where forall (s1, s2, x). x %in (s1 \\ s2) <=> ((x %in s1) and not (x %in s2))

deferred predicate %C : (set * set) ~> prop
where forall (s1, s2). (s1 %C s2) <=> (forall x. (x %in s1) => (x %in s2))

lemma mem2: forall (x, y, s). (x %in s and y %in s)
  => (x = y or y %in (s \\ singleton (x)))

lemma union_subset : forall (s1, s2). s1 %C (s1 @ s2)

lemma union_subset' : forall (s1, s2). s2 %C (s1 @ s2)

lemma flatten_union: forall (x, s1, s2, s3).
  x %in ((s1 @ s2) @ s3) <=> (x %in s1 or x %in s2 or x %in s3)

lemma flatten_union': forall (x, s1, s2, s3).
  x %in (s1 @ (s2 @ s3)) <=> (x %in s1 or x %in s2 or x %in s3)

lemma transitive_subset: forall (s1, s2, s3).
  (s1 %C s2 and s2 %C s3) => s1 %C s3

(* Inferior bound of a set. *)
predicate inf (x, s) = forall y. y %in s => x <elt y

lemma: forall (x, s1, s2). (inf (x, s1) and s2 %C s1) => inf (x, s2)
lemma: forall (x, s1, s2). (inf (x, s1 @ s2)) <=> (inf (x, s1) and inf (x, s2))
lemma: forall (x, s1, s2). (inf (x, s1) and inf (x, s2)) => inf (x, s1 ^ s2)
lemma: forall (s, x, y). (inf (x, s) and y <elt x) => inf (y, s)
lemma: forall (x, y). (inf (x, singleton (y)) <=> x <elt y)
lemma: forall (x, s). (inf (x, s) => not (x %in s))

(* Minimum of a set. *)
predicate smin (x, s) = x %in s and forall y. y %in s => (x <elt y or x = y)

lemma: forall (x, s). inf (x, s) => smin (x, s @ singleton (x))

(* The minimum is unique. *)
lemma: forall (a, m1, m2). (smin (m1, a) and smin (m2, a)) => m1 = m2

(* Superior bound of a set. *)
predicate sup (x, s) = forall y. y %in s => y <elt x

lemma: forall (x, s1, s2). (sup (x, s1) and s2 %C s1) => sup (x, s2)
lemma: forall (x, s1, s2). (sup (x, s1 @ s2)) <=> (sup (x, s1) and sup (x, s2))
lemma: forall (x, s1, s2). (sup (x, s1) and sup (x, s2)) => sup (x, s1 ^ s2)
lemma: forall (s, x, y). (sup (x, s) and x <elt y) => sup (y, s)
lemma: forall (x, y). (sup (x, singleton (y)) <=> y <elt x)
lemma: forall (x, s). (sup (x, s) => not (x %in s))

(* Maximum of a set. *)
predicate smax (x, s) = x %in s and forall y. y %in s => (x = y or y <elt x)

lemma: forall (x, s). sup (x, s) => smax (x, s @ singleton (x))

(* Extensional equality. *)
predicate === (s1, s2) = forall x. (x %in s1) <=> (x %in s2)

(* Extensionality axiom. *)
axiom: forall (s1, s2). (s1 === s2) <=> (s1 = s2)

deferred predicate disjoint : (set * set) ~> prop
where forall (s1, s2). disjoint (s1, s2) <=> ((forall y. y %in s1 => not (y %in s2)) and (forall y. y %in s2 => not (y %in s1)))

(** Trees. *)

(* Inductive type for tree. *)
type tree =
  | Empty : tree
  | Node  : (int * tree * elt * tree) -> tree

(* The abstraction of trees to sets. *)
logic elements (t) =
  | Empty -> empty
  | Node (h, l, x, r) -> elements (l) @ singleton (x) @ elements (r)

lemma disj_elements : forall (h, l, x, r, y). y %in elements (Node (h, l, x, r))
<=> (y %in elements (l) or x = y or y %in elements (r))

lemma root_in_elements: forall (h, l, x, r). x %in elements (Node (h, l, x, r))

lemma subl_in_elements: forall (h, l, x, r).
  elements (l) %C elements (Node (h, l, x, r))

lemma subr_in_elements: forall (h, l, x, r).
  elements (r) %C elements (Node (h, l, x, r))

lemma subl2_in_elements: forall (h, hl, ll, lx, lr, x, r).
    elements (ll) %C elements (Node (h, Node (hl, ll, lx, lr), x, r))
and elements (lr) %C elements (Node (h, Node (hl, ll, lx, lr), x, r))

lemma subr2_in_elements: forall (h, l, x, hr, rl, rx, rr).
  elements (rl) %C elements (Node (h, l, x, Node (hr, rl, rx, rr)))
and elements (rr) %C elements (Node (h, l, x, Node (hr, rl, rx, rr)))

(* A simple function: the emptyness test. *)
let is_empty t returns b where ((b = true) <=> (elements (t) = empty)) =
  match t with
    | Empty             -> true
    | Node (h, l, x, r) -> false
 end

(* Binary search trees. *)

inductive bst : tree ~> prop =
  | bst (Empty)
  | forall (h, l, x, r).
      bst (l) and bst (r) and sup (x, elements (l)) and inf (x, elements (r))
      => bst (Node (h, l, x, r))

predicate bst_node (l, x, r) =
   bst (l) and bst (r) and sup (x, elements (l)) and inf (x, elements (r))

lemma: forall (l, x, r). bst_node (l, x, r) =>
    ((disjoint (elements (l), elements (r)))
 and (disjoint (elements (l), singleton (x)))
 and (disjoint (elements (r), singleton (x))))

lemma: forall (s1, s2). disjoint (s1, s2) <=> disjoint (s2, s1)

lemma: forall (s1, s2, s3). (disjoint (s1, s2) and disjoint (s1, s3)) => disjoint (s1, s2 @ s3)

lemma: forall (lh, ll, lx, lr, x, rh, rl, rx, rr).
   bst_node (Node (lh, ll, lx, lr), x, Node (rh, rl, rx, rr)) =>
   (bst_node (ll, lx, lr) and bst_node (rl, rx, rr))

lemma: forall (l, x, h, rl, rx, rr).
   bst_node (l, x, Node (h, rl, rx, rr)) =>
   sup (rx, elements (l) @ singleton (x) @ elements (rl))

lemma: forall (h, ll, lx, lr, x, r).
   bst_node (Node (h, ll, lx, lr), x, r) =>
   inf (lx, elements (lr) @ singleton (x) @ elements (r))

lemma: forall (lh, ll, lx, lrh, lrl, lrx, lrr, x, r).
   bst_node (Node (lh, ll, lx, Node (lrh, lrl, lrx, lrr)), x, r) =>
   inf (lrx, elements (lrr) @ singleton (x) @ elements (r))

lemma: forall (h, l, x, rh, rlh, rll, rlx, rlr, rx, rr).
   bst_node (l, x, Node (rh, Node (rlh, rll, rlx, rlr), rx, rr)) =>
   sup (rlx, elements (l) @ singleton (x) @ elements (rll))

lemma: forall (h, l, x, r). bst (Node (h, l, x, r)) => (forall y. ((y %in elements (Node (h, l, x, r))) and y <elt x) <=> y %in elements (l))

lemma: forall (h, l, x, r). bst (Node (h, l, x, r)) => (forall y. ((y %in elements (Node (h, l, x, r))) and x <elt y) <=> y %in elements (r))

lemma: forall (h, l, x, r). bst_node (l, x, r) <=> bst (Node (h, l, x, r))

lemma: forall (h, l, x, r, y). bst_node (l, x, r) => y <elt x => not (y %in elements (r))

lemma: forall (h, l, x, r, y). bst_node (l, x, r) => x <elt y => not (y %in elements (l))

(* Membership decision procedure over binary search trees. *)

let rec mem_bst (t, x) where bst (t)
returns b where ((b = true) <=> (x %in elements (t))) =

    match t with

      | Empty ->
          false

      | Node (h, l, y, r) ->
          if (x =elt? y) then
            true
          else if (x <elt? y) then
            mem_bst (l, x)
          else
            mem_bst (r, x)

 end

(* Height. *)

logic height t =
  | Empty -> 0
  | Node (h, l, x, r) -> 1 + (max (height (l), height (r)))

(* FIXME: to be proven by lemma (by induction). *)
axiom height_positive: forall t. height (t) >= 0
lemma height_without_max: forall (h, l, x, r). height (l) < height (r) => height (Node (h, l, x, r)) = 1 + height (r)
lemma height_without_max2: forall (h, l, x, r). height (r) <= height (l) => height (Node (h, l, x, r)) = 1 + height (l)
lemma height_disj: forall (h, l, x, r). height (Node (h, l, x, r)) = height (l) + 1 or height (Node (h, l, x, r)) = height (r) + 1
lemma height_depth: forall (h, hl, hr, ll, lx, lr, x, rl, rx, rr).
height (Node (h, Node (hl, ll, lx, lr), x, Node (hr, rl, rx, rr))) =
  2 + max (max (height (ll), height (lr)), max (height (rl), height (rr)))

predicate height_of_node (l, r, h) =
    (height (l) >= height (r) and h = (height (l) + 1)) or
    (height (r) >= height (l) and h = (height (r) + 1))

lemma height_is_hl: forall (l, r, h). (height_of_node (l, r, h) and height (l) >= height (r)) => h = height (l) + 1
lemma height_is_hr: forall (l, r, h). (height_of_node (l, r, h) and height (r) >= height (l)) => h = height (r) + 1
lemma height_of_node_correct: forall (l, r). height_of_node (l, r, 1 + max (height (l), height (r)))
lemma height_of_node_correct_bis: forall (h, l, x, r). height_of_node (l, r, height (Node (h, l, x, r)))

predicate almost_height_of_node (l, r, y) =
  height_of_node (l, r, y) or height_of_node (l, r, y + 1)

lemma almost_height_of_node_max: forall (l, r, y). (almost_height_of_node (l, r, y) <=> ((y - max (height (l), height (r))) <= 1 and (y - max (height (l), height (r))) >= 0))
lemma almost_height_of_node_hl : forall (l, r, y). height (l) >= height (r) => ((almost_height_of_node (l, r, y)) <=> ((y - height (l)) <= 1 and (y - height (l)) >= 0))
lemma almost_height_of_node_hr : forall (l, r, y). height (r) >= height (l) => ((almost_height_of_node (l, r, y)) <=> ((y - height (r)) <= 1 and (y - height (r)) >= 0))

(* A tree is well-formed if the integer stored in its root node
   is its height. *)

inductive wf : tree ~> prop =
  | wf (Empty)
  | forall (h, l, x, r). h = height (Node (h, l, x, r)) and wf (l) and wf (r)
    => wf (Node (h, l, x, r))

(* We can extract the height of a well-formed tree in constant time. *)

let height? (t) where wf (t) returns h where (h = height (t)) =
  match t with
    | Empty -> 0
    | Node (h, l, x, r) -> h
  end

(* The definition of AVL trees. *)

inductive avl : tree ~> prop =
  | avl (Empty)
  | forall (h, x, l, r).
      avl (l) and avl (r) and dist (height (l), height (r), 2)
    => avl (Node (h, l, x, r))

predicate avl_node (l, r) =
  avl (l) and avl (r) and dist (height (l), height (r), 2)

lemma: forall (h, l, x, r). avl_node (l, r) <=> avl (Node (h, l, x, r))

predicate almost_avl_node (l, r) =
  avl (l) and avl (r) and dist (height (l), height (r), 3)

predicate wf_bst_avl (t) =
  wf (t) and bst (t) and avl (t)

(* Smart constructor of BST and AVL well-formed trees. *)

let mk_node (l, x, r)
where bst_node (l, x, r) and avl_node (l, r) and wf (l) and wf (r)
returns t
where (wf_bst_avl (t) and bst_node (l, x, r)
  and height_of_node (l, r, height (t))
  and height (t) = max (height (l), height (r)) + 1
  and elements (t) = (elements (l) @ singleton (x) @ elements (r))
  and t = Node (max (height (l), height (r)) + 1, l, x, r)) =
  Node (max? (height? (l), height? (r)) +? 1, l, x, r)

(* Balancing. *)
lemma union_assoc_ext : forall (s1, s2, s3). (s1 @ (s2 @ s3)) === ((s1 @ s2) @ s3)
lemma union_assoc : forall (s1, s2, s3). (s1 @ (s2 @ s3)) = ((s1 @ s2) @ s3)
lemma union_assoc5_ext : forall (s1, s2, s3, s4, s5). (s1 @ s2 @ (s3 @ s4 @ s5)) === ((s1 @ s2 @ s3) @ s4 @ s5)
lemma union_assoc5 : forall (s1, s2, s3, s4, s5). (s1 @ s2 @ (s3 @ s4 @ s5)) = ((s1 @ s2 @ s3) @ s4 @ s5)
lemma union_empty_l_ext : forall (s). (empty @ s) === s
lemma union_empty_l : forall (s). (empty @ s) = s
lemma union_empty_r_ext : forall (s). (s @ empty) === s
lemma union_empty_r : forall (s). (s @ empty) = s
lemma subset_in_ext : forall (x, s). x %in s => s === (singleton (x) @ s)
lemma subset_in : forall (x, s). x %in s => s = (singleton (x) @ s)

let bal (l, x, r)
where wf (l) and wf (r) and almost_avl_node (l, r) and bst_node (l, x, r)
returns t
where (wf (t) and avl (t) and bst (t)
  and elements (t) = (elements (l) @ singleton (x) @ elements (r))
  and (dist (height (l), height (r), 2) => height_of_node (l, r, height (t)))
  and (almost_height_of_node (l, r, height (t)))) =

  let hl = height? (l) in
  let hr = height? (r) in

    if (hl -? hr) =? 3 then let Node (h, ll, lx, lr) = l in

        if height? (lr) <=? height? (ll) then
	  mk_node (ll, lx, mk_node (lr, x, r))

        else let Node (h, lrl, lrx, lrr) = lr in
          mk_node (mk_node (ll, lx, lrl), lrx, mk_node (lrr, x, r))

    else if (hr -? hl) =? 3 then let Node (h, rl, rx, rr) = r in

        if height? (rl) <=? height? (rr) then
	  mk_node (mk_node (l, x, rl), rx, rr)

        else let Node (h, rll, rlx, rlr) = rl in
          mk_node (mk_node (l, x, rll), rlx, mk_node (rlr, rx, rr))

    else
      mk_node (l, x, r)

(* Insertion in a set. *)

predicate may_increment_height (from, to) =
  height (from) = height (to) or height (to) = height (from) + 1

lemma union_comm4_ext : forall (s1, s2, s3, s4). (s1 @ s2 @ (s3 @ s4)) === (s3 @ (s1 @ s2 @ s4))
lemma union_comm4 : forall (s1, s2, s3, s4). s1 @ s2 @ (s3 @ s4) = s3 @ (s1 @ s2 @ s4)

let rec add (x, a) where wf_bst_avl (a)
returns b
where (wf_bst_avl (b)
  and may_increment_height (a, b)
  and elements (b) = (singleton (x) @ elements (a))) =

  match a with
  | Empty ->
    Node (1, Empty, x, Empty)

  | Node (h, l, y, r) ->
	if x =elt? y then
	   a
        else if x <elt? y then
	  bal (add (x, l), y, r)
        else
	  bal (l, y, add (x, r))
 end


(* Join two trees. *)

let rec join (l, x, r)
where bst_node (l, x, r) and avl (l) and avl (r) and wf (l) and wf (r)
returns b where
        (wf_bst_avl (b)
    and (almost_height_of_node (l, r, height (b)))
    and (elements (b) = (elements (l) @ singleton (x) @ elements (r)))) =

  match l with
  | Empty ->
      add (x, r)

  | Node (lh, ll, lx, lr) ->
      match r with
	| Empty ->
	    add (x, l)
	| Node (rh, rl, rx, rr) ->
	    let lh = height? (l) in
	    let rh = height? (r) in
		if lh >? (rh +? 2) then
		  bal (ll, lx, join (lr, x, r))
		else if rh >? (lh +? 2) then
		  bal (join (l, x, rl), rx, rr)
                else
		  Node (1 +? max? (lh, rh), l, x, r)
	end
  end


(* Compute the minimal element of a non empty tree. *)
(*
lemma min_l_is_min_t: forall (h, l, x, r, y, z). bst (Node (h, l, x, r))
 => y %in elements (r) => z %in elements (l) => z <elt y

lemma min_inf: forall (x, s). smin (x, s) => inf (x, s \\ singleton (x))

let rec min_elt (t) where (not (Empty = t)) and bst (t)
returns x where smin (x, elements (t)) =
  match t with
  | Empty ->
      absurd

  | Node (h, l, x, r) ->
	match l with
	| Empty -> x
	| l -> min_elt (l)
	end
  end

lemma equiv_min:
 forall (t, x).
     (forall y. y %in elements (t) => (x <elt y or x = y))
 <=> (forall y. y %in elements (t) and not (x = y) => x <elt y)

(* Compute the maximal element of a non empty tree. *)

lemma smax_on_bst_lempty: forall (h, l, x, r).
  (bst (Node (h, l, x, r)) and r = Empty) => smax (x, elements (Node (h, l, x, r)))

let rec max_elt (t) where (not (Empty = t)) and bst (t)
returns x
where smax (x, elements (t)) =

  match t with
  | Empty -> absurd
  | Node (h, l, x, r) ->
      match r with
	| Empty -> x
	| r -> max_elt (r)
	end
  end


(* Remove the smallest element in an AVL tree. *)

predicate may_decrement_height (from, to) =
    height (from) = height (to) or height (to) = height (from) - 1

lemma diff_union_mem: forall (x, s1, s2, s3).
(x %in ((s1 @ s2) \\ s3)) <=> ((x %in s1 or x %in s2) and not (x %in s3))

lemma diff_union_mem2: forall (x, s1, s2, s3).
(x %in ((s1 \\ s3) @ (s2 \\ s3))) <=> ((x %in s1 and not (x %in s3)) or (x %in s2 and not (x %in s3)))

lemma diff_union_ext: forall (s1, s2, s3). ((s1 @ s2) \\ s3)  === ((s1 \\ s3) @ (s2 \\ s3))
lemma diff_union: forall (s1, s2, s3). ((s1 @ s2) \\ s3) = ((s1 \\ s3) @ (s2 \\ s3))

lemma diff_not_in_ext: forall (s, x). not (x %in s) => ((s \\ singleton (x)) === s)
lemma diff_not_in: forall (s, x). not (x %in s) => ((s \\ singleton (x)) = s)

lemma diff_union3_ext: forall (s1, s2, x, y). not (y %in (singleton (x) @ s2)) =>
  ((((s1 @ singleton (x) @ s2) \\ singleton (y)) === ((s1 \\ singleton (y)) @ singleton (x) @ s2))
   and (((s1 @ singleton (x) @ s2) \\ singleton (y)) = ((s1 \\ singleton (y)) @ singleton (x) @ s2)))

lemma diff_union3: forall (s1, s2, x, y). not (y %in (singleton (x) @ s2)) =>
  (((s1 @ singleton (x) @ s2) \\ singleton (y)) = ((s1 \\ singleton (y)) @ singleton (x) @ s2))

lemma diff_disjoint_union_eq_ext:
forall (s1, s2). disjoint (s2, s1) => ((s1 @ s2) \\ s1) === s2
lemma diff_disjoint_union_eq:
forall (s1, s2). disjoint (s2, s1) => ((s1 @ s2) \\ s1) = s2

lemma union_diff3_ext : forall (s1, s2, s3). disjoint (s2, s3) => ((s1 \\ s2) @ s3) === ((s1 @ s3 ) \\ s2)
lemma union_diff3 : forall (s1, s2, s3). disjoint (s2, s3) => (s1 \\ s2) @ s3 = (s1 @ s3 ) \\ s2

predicate smin_removal_ (x, a, b) = ((a \\ singleton (x)) = b and smin (x, a))
predicate smin_removal (a, b) = exists x. smin_removal_ (x, a, b)

lemma unique_min_removal: forall (x, y, a, b). smin_removal_ (x, a, b) and smin_removal_ (y, a, b) => x = y

lemma smin_prop: forall (x, l, y, r).
  bst_node (l, x, r) =>
  smin (y, elements (l)) =>
  ((not (y %in (singleton (x) @ elements (r))))
   and smin (y, elements (l) @ singleton (x) @ elements (r)))

lemma smin_on_bst: forall (l, x, r, m).
  bst_node (l, x, r) =>
  smin (m, elements (l)) => smin (m, elements (l) @ singleton (x) @ elements (r))

lemma bst_node_bis: forall (y, l, ml, x, r).
 (bst_node (l, x, r) and bst (ml) and elements (ml) = (elements (l) \\ singleton (y)))
  => bst_node (ml, x, r)

lemma smin_removal_on_bst_is_bst:
forall (l, x, r, ml).
  (bst_node (l, x, r) and smin_removal (elements (l), elements (ml)) and bst (ml)) =>
  bst_node (ml, x, r)

lemma smin_removal__on_bst: forall (l, x, r, ml, y).
  (bst_node (l, x, r) and smin_removal_ (y, elements (l), elements (ml))) =>
  (smin_removal_ (y, elements (l) @ singleton (x) @ elements (r), elements (ml) @ singleton (x) @ elements (r)))

lemma smin_removal_on_bst:  forall (l, x, r, ml).
  (bst_node (l, x, r) and smin_removal (elements (l), elements (ml))) =>
  (exists y.
     smin_removal_ (y, elements (l), elements (ml)) and
     smin_removal_ (y,
		      elements (l) @ singleton (x) @ elements (r),
		      elements (ml) @ singleton (x) @ elements (r)))

lemma smin_on_bst_lempty: forall (h, l, x, r).
  (bst (Node (h, l, x, r)) and l = Empty) => smin (x, elements (Node (h, l, x, r)))

let rec remove_min_elt (a) where wf_bst_avl (a) and not (a = Empty)
returns b
where (may_decrement_height (a, b)
  and wf_bst_avl (b)
  and smin_removal (elements (a), elements (b))) =

  match a with
  | Empty ->
    absurd

  | Node (h, l, x, r) -> assert bst_node (l, x, r) in
    match l with
        | Empty -> assert smin_removal_ (x, elements (a), elements (r)) in
            r
	| l ->
	    bal (remove_min_elt (l), x, r)
    end
  end

(* Merge two trees into one. *)

lemma stupid_def: forall (x, s).
  (x %in s) => (forall y. ((y %in s) <=> (y %in singleton (x) or y %in (s \\ singleton (x)))))

lemma diff_union_singleto_ext: forall (s, x).
  x %in s => (s === (singleton (x) @ (s \\ singleton (x))))

lemma diff_union_singleton: forall (s, x).
  x %in s => (s = (singleton (x) @ (s \\ singleton (x))))

lemma union_min_and_min_removal_ext: forall (s1, s2, x).
  (smin_removal_ (x, s1, s2) and smin (x, s1)) =>
  ((s1 === (singleton (x) @ s2)) and (s1 = (singleton (x) @ s2)))

lemma union_min_and_min_removal: forall (s1, s2, x).
  (smin_removal (s1, s2) and smin (x, s1)) =>
  (s1 = (singleton (x) @ s2))

let merge (t1, t2)
where wf_bst_avl (t1) and wf_bst_avl (t2)
and (forall (y, x). y %in elements (t1) => x %in elements (t2) => y <elt x)
and dist (height (t1), height (t2), 2)
returns t
where (wf_bst_avl (t)
  and (height (t1) > height (t2) =>
      (height (t) >= height (t1) and (height (t) - height (t1)) <= 1))
  and (height (t2) >= height (t1) =>
      (height (t) >= height (t2) and (height (t) - height (t2)) <= 1))
  and (elements (t) = (elements (t1) @ elements (t2)))) =

  match t1 with
  | Empty -> t2

  | t1 ->
      match t2 with
	| Empty -> t1
	| t2 -> bal (t1, min_elt (t2), remove_min_elt (t2))
	end
  end

(* Merge two trees into one. *)

let concat (t1, t2)
where wf_bst_avl (t1) and wf_bst_avl (t2)
and (forall (y, x). y %in elements (t1) => x %in elements (t2) => y <elt x)
returns t
where (wf_bst_avl (t) and (elements (t) = (elements (t1) @ elements (t2)))) =

  match t1 with
  | Empty ->
	t2
  | t1 ->
      match t2 with
	| Empty -> t1
	| t2 -> join (t1, min_elt (t2), remove_min_elt (t2))
	end
  end

(* Splitting. *)

lemma union_comm3_ext: forall (s1, s2, s3). ((s1 @ s2) @ s3) === ((s2 @ s1) @ s3)
lemma union_comm3: forall (s1, s2, s3). (s1 @ s2) @ s3 = (s2 @ s1) @ s3
lemma union_subsetbis_ext: forall (s1, s2). s1 %C s2 => (s2 === (s1 @ s2))
lemma union_subsetbis: forall (s1, s2). s1 %C s2 => s2 = (s1 @ s2)
lemma union3_subset: forall (s1, s2, s3). s1 %C (s1 @ s2 @ s3) and s2 %C (s1 @ s2 @ s3) and s3 %C (s1 @ s2 @ s3)
lemma diff_empty_ext: forall (s). (empty \\ s) === empty
lemma diff_empty: forall (s). (empty \\ s) = empty
lemma diff_union32_ext: forall (s1, s2, x). ((s1 @ singleton (x) @ s2) \\ singleton (x)) === (s1 @ s2)
lemma diff_union32: forall (s1, s2, x). ((s1 @ singleton (x) @ s2) \\ singleton (x)) = (s1 @ s2)

let rec split (x, t) where wf_bst_avl (t)
returns (l, r, b)
where ((b = true <=> x %in elements (t))
  and ((elements (t) \\ singleton (x)) = (elements (l) @ elements (r)))
  and wf_bst_avl (l) and wf_bst_avl (r)
  and elements (l) %C elements (t) and elements (r) %C elements (t)
  and sup (x, elements (l)) and inf (x, elements (r))) =
  match t with
  | Empty -> (Empty, Empty, false)

  | Node (h, l, y, r) ->
	if x =elt? y then
	  (l, r, true)
	else if x <elt? y then
	  let (s1, s2, pres) = split (x, l) in
          let s3 = join (s2, y, r) in
	    assert (not (x %in (singleton (y) @ elements (r)))) in
	    assert (elements (t) \\ singleton (x)) === ((elements (s1) @ elements (s2)) @ singleton (y) @ elements (r)) in
            assert elements (s2) %C elements (s3) in
 	    (s1, s3, pres)
	else
	  let (s1, s2, pres) = split (x, r) in
          let s3 = join (l, y, s1) in
            assert elements (s1) %C elements (s3) in
	    (s3, s2, pres)
  end

(* Remove *)

lemma sdiff_notin : forall (s, x). not (x %in s) => s = (s \\ singleton (x))

let rec remove (x, a) where wf_bst_avl (a)
returns b
where (wf_bst_avl (b)
  and distf (height (a), height (b)) <= 1
  and elements (b) = (elements (a) \\ singleton (x))) =

    match a with
      | Empty -> Empty
      | Node (h, l, y, r) ->
	if x =elt? y then
	  merge (l, r)
	else if x <elt? y then
	  bal (remove (x, l), y, r)
	else
	  bal (l, y, remove (x, r))
    end

(* Union *)

let rec union (a, b) where wf_bst_avl (a) and wf_bst_avl (b)
returns c
where (wf_bst_avl (c)
  and elements (c) = (elements (a) @ elements (b))) =

    match a with
      | Empty -> b
      | Node (ah, al, ax, ar) ->
	  match b with
	    | Empty -> a
	    | Node (bh, bl, bx, br) ->
		let ha = height? (a) in
		let hb = height? (b) in
		  if ha >=? hb then
		    if hb =? 1 then
			add (bx, a)
		    else
		      let (bl, br, pres) = split (ax, b) in
			assert sup (ax, elements (bl)) and inf (ax, elements (br)) in
			join (union (al, bl), ax, union (ar, br))
		  else
		    if ha =? 1 then
			add (ax, b)
		    else
		      let (al, ar, pres) = split (bx, a) in
			assert sup (bx, elements (al)) and inf (bx, elements (ar)) in
			join (union (al, bl), bx, union (ar, br))
	end
  end


(* Intersection *)

lemma inter_empty: forall s. empty ^ s = empty
lemma inter_empty_bis: forall s. s ^ empty = empty
lemma inter_union: forall (s1, x, s2, t1, t2, b).
   b = t1 @ singleton (x) @ t2 =>
   (s1 @ singleton (x) @ s2) ^ b = (t1 ^ s1) @ singleton (x) @ (t2 ^ s2)

let rec inter (a, b) where wf_bst_avl (a) and wf_bst_avl (b)
returns c
where (wf_bst_avl (c) and elements (c) = (elements (a) ^ elements (b))) =

    match a with
      | Empty -> Empty
      | Node (ah, al, ax, ar) ->
	  match b with
	    | Empty -> Empty
	    | Node (bh, bl, bx, br) ->
		let (bl, br, pres) = split (ax, b) in
                  assert (sup (ax, elements (bl))) and (inf (ax, elements (br))) in
		  if pres then
		    join (inter (al, bl), ax, inter (ar, br))
		  else
		    concat (inter (al, bl), inter (ar, br))
         end
  end

(* Substraction *)

let rec diff (a, b) where wf_bst_avl (a) and wf_bst_avl (b)
returns c
where (wf_bst_avl (c) and elements (c) = (elements (a) \\ elements (b))) =

  match a with
  | Empty -> Empty
  | Node (ah, al, ax, ar) ->
      match b with
	| Empty -> a
	| Node (bh, bl, bx, br) ->
	    let (bl, br, pres) = split (ax, b) in
	      if pres then
		concat (diff (al, bl), diff (ar, br))
	      else
		join (diff (al, bl), ax, diff (ar, br))
	end
  end

(* Subset decision. *)

let rec subset (a, b) where bst (a) and bst (b)
returns c where (c = true <=> elements (a) %C elements (b)) =

    match a with
      | Empty ->
	  true

      | Node (ah, al, ax, ar) ->
	  match b with
	    | Empty -> false
	    | Node (bh, bl, bx, br) ->
		if ax =elt? bx then
		  subset (al, bl) & subset (ar, br)
		else if ax <elt? bx then
		  subset (Node (ah, al, ax, Empty), bl) & subset (ar, b)
		else
		  subset (Node (ah, Empty, ax, ar), br) & subset (al, b)
	end
  end
*)
